
/**
 * Copyright 2009 cestum.org
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */

package org.waveprotocol.wave.model.document.operation.automaton {

import org.waveprotocol.wave.model.document.operation.AnnotationBoundaryMap;
import org.waveprotocol.wave.model.document.operation.Attributes;
import org.waveprotocol.wave.model.document.operation.AttributesUpdate;
import org.waveprotocol.wave.model.document.operation.automaton.doc.EmptyAutomationDoc;
import org.waveprotocol.wave.model.document.operation.automaton.enums.AnyPC;
import org.waveprotocol.wave.model.document.operation.automaton.enums.BlipTextPC;
import org.waveprotocol.wave.model.document.operation.automaton.enums.NonePC;
import org.waveprotocol.wave.model.document.operation.automaton.enums.PermittedCharacters;
import org.waveprotocol.wave.model.document.operation.automaton.violation.OperationIllFormed;
import org.waveprotocol.wave.model.document.operation.automaton.violation.OperationInvalid;
import org.waveprotocol.wave.model.document.operation.automaton.violation.SchemaViolation;
import org.waveprotocol.wave.model.document.operation.automaton.violation.ViolationCollector;
import org.waveprotocol.wave.model.document.operation.impl.AnnotationMap;
import org.waveprotocol.wave.model.document.operation.impl.AnnotationMapImpl;
import org.waveprotocol.wave.model.document.operation.impl.AnnotationsUpdateImpl;
import org.waveprotocol.wave.model.document.operation.util.StateMap;
import org.waveprotocol.wave.model.util.Preconditions;
import org.waveprotocol.wave.model.util.StrUtil;
import org.waveprotocol.wave.model.util.Utf16Util;
import org.goverla.collections.ArrayList;



/**
 * Comments from wave-protocol src=>
 * A state machine that can be used to accept or generate valid or invalid document
 * operations.
 *
 * The basic usage model is as follows: An automaton is parameterized by a
 * document and a set of constraints based on an XML schema, and will
 * accept/generate all valid operations for that document and those constraints.
 *
 * Every possible operation component (such as "elementStart(...)") corresponds
 * to a potential transition of the automaton.  The checkXXX methods
 * (such as checkElementStart(...)) determine whether a given transition exists
 * and is valid, or whether it is invalid, or ill-formed.  The doXXX methods
 * will perform the transition.  Ill-formed transitions must not be performed.
 * Invalid transitions are permitted, but after performing an invalid transition,
 * the validity of the operation components that follow is not well-defined.
 *
 * The checkFinish() method determines whether ending an operation is acceptable
 * (or whether any opening components are missing the corresponding closing
 * component or similar).
 *
 * The checkXXX methods accept a ViolationCollector object where they will record
 * details about any violations.  If a proposed transition is invalid for more
 * than one reason, the checkXXX method may detect only one (or any subset) of
 * the reasons and record only those violations.  The ViolationCollector parameter
 * may also be null, in which case details about the violations will not be
 * recorded.
 *
 * To validate an operation, the automaton needs to be driven according to
 * the operation components in that operation.  DocOpValidator does
 * this.
 *
 * To generate a random operation, the automaton needs to be driven based on
 * a random document operation component generator.  RandomDocOpGenerator does
 * this.
 */
// TODO: size limits
public final class DocOpAutomaton {
	
	static var EXPENSIVE_ASSERTIONS:Boolean = false;
	
	//For overloaded add methods
	public function addViolation(a:ViolationCollector, v:Violation):ValidationResult {  
		if (v instanceof OperationIllFormed) {  
			return addViolationIllFormed(a,OperationIllFormed(v) );  
		} else if (v instanceof OperationInvalid) {  
			return addViolationInvalid(a,OperationInvalid(v));  
		} else if (v instanceof SchemaViolation) {  
			return addViolationSchema(a,SchemaViolation(v));  
		} 
		return ValidationResult.INVALID_DOCUMENT;
	}  
	
	
	
	
	private function addViolationIllFormed(a:ViolationCollector, v:OperationIllFormed):ValidationResult {
		if (a != null) {
			a.add(v);
		}
		return v.validationResult();
	}
	
	private function addViolationInvalid(a:ViolationCollector, v:OperationInvalid):ValidationResult {
		if (a != null) {
			a.add(v);
		}
		return v.validationResult();
	}
	
	private function addViolationSchema(a:ViolationCollector, v:SchemaViolation):ValidationResult {
		if (a != null) {
			a.add(v);
		}
		return v.validationResult();
	}
	
	private function illFormedOperation(description:String):OperationIllFormed {
		return new OperationIllFormed(description, effectivePos, resultingPos);
	}
	
	private function invalidOperation(description:String):OperationInvalid {
		return new OperationInvalid(description, effectivePos, resultingPos);
	}
	
	private function schemaViolation(description:String):SchemaViolation {
		return new SchemaViolation(description, effectivePos, resultingPos);
	}
	
	function valid():ValidationResult {
		return ValidationResult.VALID;
	}
	
	function mismatchedInsertStart(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("elementStart with no matching elementEnd"));
	}
	
	function mismatchedDeleteStart(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation(
			"deleteElementStart with no matching deleteElementEnd"));
	}
	
	function mismatchedInsertEnd(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("elementEnd with no matching elementStart"));
	}
	
	function mismatchedDeleteEnd(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation(
			"deleteElementEnd with no matching deleteElementStart"));
	}
	
	function mismatchedStartAnnotation(v:ViolationCollector, key:String):ValidationResult {
		return addViolation(v, illFormedOperation("annotation of key " + key
			+ " starts but never ends"));
	}
	
	function mismatchedEndAnnotation(v:ViolationCollector, key:String):ValidationResult {
		return addViolation(v, illFormedOperation("annotation of key " + key
			+ " ends without having started"));
	}
	
	private function retainItemCountNotPositive(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("retain item count not positive"));
	}
	
	private function retainInsideInsertOrDelete(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("retain inside insert or delete"));
	}
	
	private function attributeChangeInsideInsertOrDelete(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("attribute change inside insert or delete"));
	}
	
	private function retainPastEnd(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("retain past end of document"));
	}
	
	private function missingRetainToEnd(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("operation shorter than document"));
	}
	
	private function nullCharacters(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("characters is null"));
	}
	
	private function emptyCharacters(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("characters is empty"));
	}
	
	private function insertInsideDelete(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("insertion inside deletion"));
	}
	
	private function deleteInsideInsert(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("deletion inside insertion"));
	}
	
	private function nullTag(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("element type is null"));
	}
	
	private function nullAttributes(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("attributes is null"));
	}
	
	private function nullAttributeKey(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("attribute key is null"));
	}
	
	private function nullAttributeValue(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("attribute value is null"));
	}
	
	private function nullAttributesUpdate(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("attributes update is null"));
	}
	
	private function attributeKeysNotStrictlyMonotonic(v:ViolationCollector,
													   key1:String, key2:String):ValidationResult {
		return addViolation(v, illFormedOperation("attribute keys not strictly monotonic: "
			+ key1 + " >= " + key2));
	}
	
	private function annotationKeysNotStrictlyMonotonic(v:ViolationCollector,
														key1:String, key2:String):ValidationResult {
		return addViolation(v, illFormedOperation("annotation keys not strictly monotonic: "
			+ key1 + " >= " + key2));
	}
	
	private function nullAnnotationKey(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("annotation key is null"));
	}
	
	private function invalidCharacterInAnnotationKey(v:ViolationCollector, key:String):ValidationResult {
		return addViolation(v, illFormedOperation("invalid character in annotation key: " + key));
	}
	
	private function annotationKeyNotValidUtf16(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("annotation key is not valid UTF-16"));
	}
	
	private function annotationValueNotValidUtf16(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("annotation value is not valid UTF-16"));
	}
	
	private function charactersContainsSurrogate(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("characters component contains surrogate"));
	}
	
	private function deleteCharactersContainsSurrogate(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("delete characters component contains surrogate"));
	}
	
	private function charactersInvalidUnicode(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("characters component contains invalid unicode"));
	}
	
	private function deleteCharactersInvalidUnicode(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("delete characters component contains invalid unicode"));
	}
	
	private function attributeNameNotXmlName(v:ViolationCollector, name:String):ValidationResult {
		return addViolation(v, illFormedOperation("attribute name is not an XML Name: \""
			+ name + "\""));
	}
	
	private function attributeValueNotValidUtf16(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("attribute value is not valid UTF-16"));
	}
	
	private function elementTypeNotXmlName(v:ViolationCollector, name:String):ValidationResult {
		return addViolation(v, illFormedOperation("element type is not an XML Name: \""
			+ name + "\""));
	}
	
	private function duplicateAnnotationKey(v:ViolationCollector, key:String):ValidationResult {
		return addViolation(v, illFormedOperation("annotation boundary contains duplicate key "
			+ key));
	}
	
	private function adjacentAnnotationBoundaries(v:ViolationCollector):ValidationResult {
		return addViolation(v, illFormedOperation("adjacent annotation boundaries"));
	}
	
	private function textNotAllowedInElement(v:ViolationCollector, tag:String):ValidationResult {
		return addViolation(v, schemaViolation("element type " + tag
			+ " does not allow text content"));
	}
	
	private function onlyBlipTextAllowedInElement(v:ViolationCollector, tag:String):ValidationResult {
		return addViolation(v, schemaViolation("element type " + tag
			+ " only allows blip text content, not arbitrary characters"));
	}
	
	private function cannotDeleteSoManyCharacters(v:ViolationCollector,
												  available:int, chars:String):ValidationResult {
		var attempted:int= chars.length;
		return addViolation(v, invalidOperation("cannot delete " + attempted + " characters,"
			+ " only " + available + " available"));
	}
	
	private function invalidAttribute(v:ViolationCollector, type:String, attr:String,
									  value:String):ValidationResult {
		return addViolation(v, schemaViolation("type " + type + " does not permit attribute "
			+ attr + " with value " + value));
	}
	
	private function invalidChild(v:ViolationCollector, parentTag:String, childTag:String):ValidationResult {
		if (parentTag == null) {
			return addViolation(v, schemaViolation("element type " + childTag
				+ " not permitted at top level"));
		} else {
			return addViolation(v, schemaViolation("element type " + parentTag
				+ " does not permit subelement type " + childTag));
		}
	}
	
	private function differentElementTypeRequired(v:ViolationCollector, expectedType:String,
												  actualType:String):ValidationResult {
		return addViolation(v, schemaViolation("element of type " + expectedType
			+ " required, not " + actualType));
	}
	
	private function childElementRequired(v:ViolationCollector, expectedType:String):ValidationResult {
		return addViolation(v, schemaViolation("child element required, expected type "
			+ expectedType));
	}
	
	private function attemptToDeleteRequiredChild(v:ViolationCollector):ValidationResult {
		return addViolation(v, schemaViolation("attempt to delete required child"));
	}
	
	private function attemptToInsertBeforeRequiredChild(v:ViolationCollector):ValidationResult {
		return addViolation(v, schemaViolation("attempt to insert before required child"));
	}
	
	private function noElementStartToDelete(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("no element start to delete here"));
	}
	
	private function noElementEndToDelete(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("no element end to delete here"));
	}
	
	private function noElementStartToChangeAttributes(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("no element start to change attributes here"));
	}
	
	private function oldAnnotationsDifferFromDocument(v:ViolationCollector,
													  oldValue:String, valueInDoc:String):ValidationResult {
		return addViolation(v, invalidOperation("old annotations differ from document: "
			+ " purported old value is " + oldValue + ", actual value in document is " + valueInDoc));
	}
	
	private function newAnnotationsIncorrectForDeletion(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("new annotation value incorrect for deletion"));
	}
	
	private function oldTagDifferFromDocument(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("old element type differs from document"));
	}
	
	private function oldAttributesDifferFromDocument(v:ViolationCollector):ValidationResult {
		return addViolation(v, invalidOperation("old attributes differ from document"));
	}
	
	private function missingAnnotationForDeletion(v:ViolationCollector, key:String,
												  valueInDoc:String, requiredValue:String):ValidationResult {
		return addViolation(v, invalidOperation("deletion does not reset value for key "
			+ key + " from " + valueInDoc + " to " + requiredValue));
	}
	
	private function oldCharacterDiffersFromDocument(v:ViolationCollector,
													 expected:String, actual:String):ValidationResult {
		return addViolation(v, invalidOperation("attempt to delete character " + actual
			+ " when the actual character is " + expected));
	}
	
	
	
	
	
	private function elementStartingHere():String {
		Preconditions.checkPositionIndex(effectivePos, doc.length());
		return doc.elementStartingAt(effectivePos);
	}
	
	private function elementEndingNext():String {
		Preconditions.checkPositionIndex(effectivePos, doc.length());
		return doc.elementEndingAt(effectivePos);
	}
	
	// tag==null means text allowed at top level
	private function permittedCharacters(type:String):PermittedCharacters {
		return constraints.permittedCharacters(type);
	}
	
	private function elementAllowsAttribute(type:String, attributeName:String, attributeValue:String):Boolean {
		return constraints.permitsAttribute2(type, attributeName, attributeValue);
	}
	
	// parentType==null means childType allowed at top level
	private function elementAllowsChild(parentType:String, childType:String):Boolean {
		return constraints.permitsChild(parentType, childType);
	}
	
	// returns either null or the type of the first required child
	private function requiredFirstChild(parentType:String):String {
		var list:ArrayList= constraints.getRequiredInitialChildren(parentType);
		if (list.length ==0 ) {
			return null;
		} else if (list.length > 1) {
			throw new Error("Schema requires multiple initial children");
		} else {
			return String(list.getItemAt(0));
		}
	}
	
	
	private var doc:AutomatonDocument;
	private var constraints:DocumentSchema;
	
	
	// current state
	
	private var effectivePos:int= 0;
	// first item is bottom of stack, last is top
	
	private var insertionStack:ArrayList;
	private var nextRequiredElement:String= null;
	private var deletionStackDepth:int= 0;
	private var annotationsUpdate:AnnotationsUpdateImpl= new AnnotationsUpdateImpl(null);
	private var afterAnnotationBoundary:Boolean= false;
	// This can become null if the operation is invalid.
	private var targetAnnotationsForDeletion:AnnotationMap= EMPTY_ANNOTATIONS;
	// more state to track just to be able to produce better diagnostic messages
	private var resultingPos:int= 0;
	public static var EMPTY_DOCUMENT:AutomatonDocument= new EmptyAutomationDoc();
	
	/**
	 * Creates an automaton that corresponds to the set of all possible operations
	 * on the given document under the given schema constraints.
	 */
	public function DocOpAutomaton(doc:AutomatonDocument, constraints:DocumentSchema) {
		this.doc = doc;
		this.constraints = constraints;
		this.nextRequiredElement = requiredFirstChild(null);
		this.insertionStack = new ArrayList();
	}
	
	
	/**
	 * Copy Constructor
	 */
	public static function getDocOpAutomationCopy(other:DocOpAutomaton):DocOpAutomaton {
		return  DocOpAutomaton.getDocOpAutomationCopy2(other, other.constraints);
	}
	
	/**
	 * Copy Constructor 2
	 */
	public static function getDocOpAutomationCopy2(other:DocOpAutomaton,
												   constraints:DocumentSchema):DocOpAutomaton {
		var d:DocOpAutomaton= new DocOpAutomaton(other.doc, constraints);
		d.afterAnnotationBoundary = other.afterAnnotationBoundary;
		d.annotationsUpdate = other.annotationsUpdate;
		d.deletionStackDepth = other.deletionStackDepth;
		d.effectivePos = other.effectivePos;
		//d.insertionStack = new ArrayList<InsertStart>(other.insertionStack);
		d.nextRequiredElement = other.nextRequiredElement;
		d.resultingPos = other.resultingPos;
		d.targetAnnotationsForDeletion = other.targetAnnotationsForDeletion;
		return d;
	}
	
	// current state primitive readers
	
	private function effectiveDocSymbol():int {
		if (effectivePos >= doc.length()) {
			return DocSymbol.END;
		}
		{
			var s:String= elementStartingHere();
			if (s != null) {
				return DocSymbol.OPEN;
			}
		}
		{
			var s:String= elementEndingNext();
			if (s != null) {
				return DocSymbol.CLOSE;
			}
		}
		return DocSymbol.CHARACTER;
	}
	
	// only defined for open and close
	private function effectiveDocSymbolTag():String {
		switch (effectiveDocSymbol()) {
			case DocSymbol.OPEN: {
				var tag:String= elementStartingHere();
				org.waveprotocol.wave.model.util.Assert.assert(tag != null);
				return tag;
			}
			case DocSymbol.CLOSE: {
				var tag:String= elementEndingNext();
				org.waveprotocol.wave.model.util.Assert.assert(tag != null);
				return tag;
			}
			default:
				throw new Error("Illegal Access: not at element start or end");
		}
	}
	
	// only defined for open
	private function effectiveDocSymbolAttributes():Attributes {
		switch (effectiveDocSymbol()) {
			case DocSymbol.OPEN: {
				var attributes:Attributes= doc.attributesAt(effectivePos);
				org.waveprotocol.wave.model.util.Assert.assert(attributes != null);
				return attributes;
			}
			default:
				throw new Error("Illegal State: not at element start");
		}
	}
	
	private function insertionStackIsEmpty():Boolean {
		return (insertionStack.length == 0);
	}
	
	private function deletionStackIsEmpty():Boolean {
		return deletionStackDepth == 0;
	}
	
	// null if at top level
	private function effectiveEnclosingElementTag():String {
		// This procedure will find the element at depth == 0.
		var depth:int= 0;
		for (var i:int= insertionStack.length - 1; i >= 0; i--) {
			var e:InsertStart= InsertStart(insertionStack.getItemAt(i));
			if (depth == 0) { return e.tag; }
			depth--;
		}
		if (effectivePos > doc.length()) { return null; }
		return doc.nthEnclosingElementTag(effectivePos, depth);
	}
	
	/**
	 * Returns the maximum permitted retain item count, assuming that a retain
	 * component is valid.
	 */
	public function maxRetainItemCount():int {
		if (effectivePos >= doc.length()) {
			return 0;
		} else {
			return doc.length() - effectivePos;
		}
	}
	
	public function currentElementStartTag():String {
		return doc.elementStartingAt(effectivePos);
	}
	
	public function currentElementStartAttributes():Attributes {
		return doc.attributesAt(effectivePos);
	}
	
	public function currentAnnotations():AnnotationMap {
		if (effectivePos >= doc.length()) {
			return EMPTY_ANNOTATIONS;
		} else {
			return doc.annotationsAt(effectivePos);
		}
	}
	
	public function nextChar(offset:int):int {
		Preconditions.checkArgument(offset >= 0, "Offset must be positive");
		if (offset >= doc.length() - effectivePos) { return -1; }
		return doc.charAt(effectivePos + offset);
	}
	
	/**
	 * Non-negative.  0 means neutral.  Larger values mean more complexity.
	 */
	public function insertionStackComplexityMeasure():int {
		return insertionStack.length;
	}
	
	/**
	 * Non-negative.  0 means neutral.  Larger values mean more complexity.
	 */
	public function deletionStackComplexityMeasure():int {
		return deletionStackDepth;
	}
	
	public function openAnnotations():ArrayList {
		var r:ArrayList= new ArrayList();
		for (var i:int= 0; i < annotationsUpdate.changeSize(); i++) {
			r.addItem(annotationsUpdate.getChangeKey(i));
		}
		return r;
	}
	
	private function canRetain(itemCount:int):Boolean {
		org.waveprotocol.wave.model.util.Assert.assert(itemCount >= 0);
		return itemCount <= maxRetainItemCount();
	}
	
	/**
	 * If a deleteCharacters operation component is permitted as the next
	 * component, returns the maximum number of characters that it can delete.
	 * Otherwise, the return value is undefined.
	 */
	public function maxCharactersToDelete():int {
		if (effectivePos >= doc.length()) {
			return 0;
		}
		return doc.remainingCharactersInElement(effectivePos);
	}
	
	
	// current state manipulators
	
	private function advance(distance:int):void {
		// we're not asserting canIncreaseLength() or similar here, since
		// the driver may be generating an invalid op deliberately.
		org.waveprotocol.wave.model.util.Assert.assert(distance >= 0);
		effectivePos += distance;
	}
	
	private function insertionStackPush(e:InsertStart):void {
		insertionStack.addItem(e);
	}
	
	private function deletionStackPush():void {
		deletionStackDepth++;
	}
	
	private function insertionStackPop():void {
		org.waveprotocol.wave.model.util.Assert.assert(!insertionStack.length == 0);
		insertionStack.removeItemAt(insertionStack.length - 1);
	}
	
	private function deletionStackPop():void {
		org.waveprotocol.wave.model.util.Assert.assert(!deletionStackIsEmpty());
		deletionStackDepth--;
	}
	
	
	private static function equal(a:Object, b:Object):Boolean {
		return a == null ? b == null : a.equals(b);
	}
	
	
	// check/do methods
	
	private function checkAnnotationsForRetain(v:ViolationCollector, itemCount:int):ValidationResult {
		for (var i:int= 0; i < annotationsUpdate.changeSize(); i++) {
			var key:String= annotationsUpdate.getChangeKey(i);
			var oldValue:String= annotationsUpdate.getOldValue(i);
			var firstChange:int= doc.firstAnnotationChange(effectivePos, effectivePos + itemCount,
				key, oldValue);
			if (firstChange != -1) {
				return oldAnnotationsDifferFromDocument(v, oldValue, doc.getAnnotation(firstChange, key));
			}
		}
		return valid();
	}
	
	public function checkRetain(itemCount:int, v:ViolationCollector):ValidationResult {
		// well-formedness
		if (itemCount <= 0) { return retainItemCountNotPositive(v); }
		if (!insertionStackIsEmpty()) { return retainInsideInsertOrDelete(v); }
		if (!deletionStackIsEmpty()) { return retainInsideInsertOrDelete(v); }
		// validity
		if (!canRetain(itemCount)) { return retainPastEnd(v); }
		return checkAnnotationsForRetain(v, itemCount);
	}
	
	public function doRetain(itemCount:int):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(checkRetain(itemCount, null) != ValidationResult.ILL_FORMED);
		}
		advance(itemCount);
		updateDeletionTargetAnnotations();
		resultingPos += itemCount;
		afterAnnotationBoundary = false;
	}
	
	
	private function validateAnnotationKey(key:String, v:ViolationCollector):ValidationResult {
		if (key == null) { return nullAnnotationKey(v); }
		if (key.indexOf("?") > 0|| key.indexOf("@") >0) { return invalidCharacterInAnnotationKey(v, key); }
		if (!Utf16Util.isValidUtf16(key)) { return annotationKeyNotValidUtf16(v); }
		return ValidationResult.VALID;
	}
	
	private function validateAnnotationValue(value:String, v:ViolationCollector):ValidationResult {
		if (value == null) { return ValidationResult.VALID; }
		if (!Utf16Util.isValidUtf16(value)) { return annotationValueNotValidUtf16(v); }
		return ValidationResult.VALID;
	}
	
	
	public function checkAnnotationBoundary(map:AnnotationBoundaryMap,
											v:ViolationCollector):ValidationResult {
		// well-formedness
		if (afterAnnotationBoundary) { return adjacentAnnotationBoundaries(v); }
		var endKeys:ArrayList= new ArrayList();
		for (var i:int= 0; i < map.endSize(); i++) {
			var key:String= map.getEndKey(i);
			{
				var r:ValidationResult= validateAnnotationKey(key, v);
				if (!r.isValid()) { return r; }
			}
			if (i > 0 && key <= map.getEndKey(i - 1) ) {
				return annotationKeysNotStrictlyMonotonic(v, map.getEndKey(i - 1), key);
			}
			if (!annotationsUpdate.containsKey(key)) { return mismatchedEndAnnotation(v, key); }
			endKeys.addItem(key);
		}
		for (var i:int= 0; i < map.changeSize(); i++) {
			var key:String= map.getChangeKey(i);
			{
				var r:ValidationResult= validateAnnotationKey(key, v);
				if (!r.isValid()) { return r; }
			}
			{
				var r:ValidationResult= validateAnnotationValue(map.getOldValue(i), v);
				if (!r.isValid()) { return r; }
			}
			{
				var r:ValidationResult= validateAnnotationValue(map.getNewValue(i), v);
				if (!r.isValid()) { return r; }
			}
			if (i > 0 && key <= map.getChangeKey(i - 1)) {
				return annotationKeysNotStrictlyMonotonic(v, map.getChangeKey(i - 1), key);
			}
			if (endKeys.contains(key)) { return duplicateAnnotationKey(v, key); }
		}
		return valid();
	}
	
	public function doAnnotationBoundary(map:AnnotationBoundaryMap):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkAnnotationBoundary(map, null).isIllFormed());
		}
		annotationsUpdate = annotationsUpdate.composeWithAnnotationBoundary(map) as AnnotationsUpdateImpl;
		afterAnnotationBoundary = true;
	}
	
	
	private static var EMPTY_ANNOTATIONS:AnnotationMap= AnnotationMapImpl.EMPTY_MAP;
	
	public function inheritedAnnotations():AnnotationMap {
		if (effectivePos == 0|| effectivePos > doc.length()) {
			return EMPTY_ANNOTATIONS;
		} else {
			var posToInheritFrom:int= effectivePos - 1;
			return doc.annotationsAt(posToInheritFrom);
		}
	}
	
	private function updateDeletionTargetAnnotations():void {
		if (effectivePos > doc.length()) {
			targetAnnotationsForDeletion = null;
		} else {
			targetAnnotationsForDeletion =
				inheritedAnnotations().updateWithNoCompatibilityCheck(annotationsUpdate);
		}
	}
	
	private function checkAnnotationsForInsertion(v:ViolationCollector):ValidationResult {
		if (effectivePos > doc.length()) {
			// Invalid operation, nothing to check.
			return valid();
		}
		var posToInheritFrom:int= effectivePos - 1;
		for (var i:int= 0; i < annotationsUpdate.changeSize(); i++) {
			var key:String= annotationsUpdate.getChangeKey(i);
			var oldValue:String= annotationsUpdate.getOldValue(i);
			var defaultFromDocument:String= posToInheritFrom == -1? null :
				doc.getAnnotation(posToInheritFrom, key);
			if (!equal(oldValue, defaultFromDocument)) {
				return oldAnnotationsDifferFromDocument(v, oldValue, defaultFromDocument);
			}
		}
		return valid();
	}
	
	private function checkForInsertionBeforeRequiredChild(v:ViolationCollector):ValidationResult {
		if (effectivePos < doc.length() && insertionStackIsEmpty()) {
			var parentType:String= doc.nthEnclosingElementTag(effectivePos, 0);
			var requiredFirstChild:String= requiredFirstChild(parentType);
			var isFirstChild:Boolean= effectivePos == 0|| doc.elementStartingAt(effectivePos - 1) != null;
			if (isFirstChild && requiredFirstChild != null) {
				return attemptToInsertBeforeRequiredChild(v);
			}
		}
		return ValidationResult.VALID;
	}
	
	public function checkCharacters(chars:String, v:ViolationCollector):ValidationResult {
		// well-formedness
		if (chars == null) { return nullCharacters(v); }
		if (StrUtil.isEmpty(chars)) { return emptyCharacters(v); }
		if (Utf16Util.firstSurrogate(chars) != -1) { return charactersContainsSurrogate(v); }
		if (!Utf16Util.isValidUtf16(chars)) { return charactersInvalidUnicode(v); }
		if (!deletionStackIsEmpty()) { return insertInsideDelete(v); }
		// validity
		{
			var r:ValidationResult= checkAnnotationsForInsertion(v);
			if (!r.isValid()) { return r; }
		}
		// schema
		if (nextRequiredElement != null) {
			childElementRequired(v, nextRequiredElement);
		}
		{
			var r:ValidationResult= checkForInsertionBeforeRequiredChild(v);
			if (!r.isValid()) { return r; }
		}
		var enclosingTag:String= effectiveEnclosingElementTag();
		var p:PermittedCharacters= permittedCharacters(enclosingTag);
		if (p instanceof NonePC) {
			return textNotAllowedInElement(v, enclosingTag);
		} else if (p instanceof BlipTextPC) {
			if (!Utf16Util.isGoodUtf16ForBlip(chars)) {
				return onlyBlipTextAllowedInElement(v, enclosingTag);
			}
		} else if (p instanceof AnyPC) {
			
		} else {
			throw new Error("unexpected return value from permittedCharacters()");
		}
		//    switch (permittedCharacters(enclosingTag)) {
		//      case PermittedCharacters.NONE:
		//        return textNotAllowedInElement(v, enclosingTag);
		//      case BlipTextPC:
		//        if (!Utf16Util.isGoodUtf16ForBlip(chars)) {
		//          return onlyBlipTextAllowedInElement(v, enclosingTag);
		//        }
		//        break;
		//      case BlipTextPC:
		//        break;
		//      default:
		//        throw new AssertionError("unexpected return value from permittedCharacters()");
		//    }
		return valid();
	}
	
	public function doCharacters(characters:String):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(checkCharacters(characters, null) != ValidationResult.ILL_FORMED);
		}
		updateDeletionTargetAnnotations();
		resultingPos += characters.length;
		afterAnnotationBoundary = false;
	}
	
	
	private function checkAnnotationsForDeletion(v:ViolationCollector, itemCount:int):ValidationResult {
		if (targetAnnotationsForDeletion == null) {
			// Invalid operation, nothing to check.
			return valid();
		}
		
		// Check that all annotations contained in the update have correct old and
		// new values.
		for (var i:int= 0; i < annotationsUpdate.changeSize(); i++) {
			var key:String= annotationsUpdate.getChangeKey(i);
			var oldValue:String= annotationsUpdate.getOldValue(i);
			var firstChange:int= doc.firstAnnotationChange(effectivePos, effectivePos + itemCount,
				key, oldValue);
			if (firstChange != -1) {
				return oldAnnotationsDifferFromDocument(v, oldValue, doc.getAnnotation(firstChange, key));
			}
			var newValue:String= annotationsUpdate.getNewValue(i);
			if (!equal(newValue, targetAnnotationsForDeletion.getValue(key))) {
				return newAnnotationsIncorrectForDeletion(v);
			}
		}
		// TODO: Find a way to speed this up.
		for (var offset:int= 0; offset < itemCount; offset++) {
			var pos:int= effectivePos + offset;
			var annotationsHere:StateMap= doc.annotationsAt(pos);
			// Check that the update contains all values that need to be set; the set of
			// keys to check is the union of keys at the current position and at the
			// position that it would inherit from.
			for (var key:String in annotationsHere.keySet()) {
				var valueInDoc:String= annotationsHere.getValue(key);
				var requiredValue:String= String(targetAnnotationsForDeletion.getValue(key));
				if (!equal(valueInDoc, requiredValue)) {
					if (!annotationsUpdate.containsKey(key)) {
						return missingAnnotationForDeletion(v, key, valueInDoc, requiredValue);
					}
				}
			}
			for (var key:String in targetAnnotationsForDeletion.keySet()) {
				var valueInDoc:String= annotationsHere.getValue(key);
				var requiredValue:String= targetAnnotationsForDeletion.getValue(key);
				if (!equal(valueInDoc, requiredValue)) {
					if (!annotationsUpdate.containsKey(key)) {
						return missingAnnotationForDeletion(v, key, valueInDoc, requiredValue);
					}
				}
			}
		}
		return valid();
	}
	
	
	private function checkAttributesWellFormed(attr:Attributes, v:ViolationCollector):ValidationResult {
		if (attr == null) { return nullAttributes(v); }
		var previousKey:String= null;
		//    Map<String, String> a = attr;
		var size:int = attr.keySet().length;
		for (var x:int=0; x< size; x++) {
			var key:String = attr.keySet()[x] as String;
			if (key == null) { return nullAttributeKey(v); }
			if (!Utf16Util.isXmlName(key)) { return attributeNameNotXmlName(v, key); }
			if (attr.getValue(key) == null) { return nullAttributeValue(v); }
			if (!Utf16Util.isValidUtf16(key)) { return attributeValueNotValidUtf16(v); }
			if (previousKey != null && previousKey.localeCompare(key) >= 0) {
				return attributeKeysNotStrictlyMonotonic(v, previousKey, key);
			}
			previousKey = key;
		}
		return ValidationResult.VALID;
	}
	
	private function checkAttributesUpdateWellFormed(u:AttributesUpdate,
													 v:ViolationCollector):ValidationResult {
		if (u == null) { return nullAttributesUpdate(v); }
		var previousKey:String= null;
		for (var i:int= 0; i < u.changeSize(); i++) {
			var key:String= u.getChangeKey(i);
			if (key == null) { return nullAttributeKey(v); }
			if (!Utf16Util.isXmlName(key)) { return attributeNameNotXmlName(v, key); }
			if (previousKey != null && previousKey.localeCompare(key) >= 0) {
				return attributeKeysNotStrictlyMonotonic(v, previousKey, key);
			}
			if (u.getOldValue(i) != null && !Utf16Util.isValidUtf16(u.getOldValue(i))) {
				return attributeValueNotValidUtf16(v);
			}
			if (u.getNewValue(i) != null && !Utf16Util.isValidUtf16(u.getNewValue(i))) {
				return attributeValueNotValidUtf16(v);
			}
			previousKey = key;
		}
		return ValidationResult.VALID;
	}
	
	private function validateAttributes(tag:String, attr:Attributes, v:ViolationCollector):ValidationResult {
		//	Map<String, String> a = attr;
		for (var key:String in attr.keySet()) {
			var value:String= String(attr.getValue(key));
			if (!elementAllowsAttribute(tag, key, value)) {
				return invalidAttribute(v, tag, key, value);
			}
		}
		return ValidationResult.VALID;
	}
	
	
	public function checkElementStart(type:String, attr:Attributes, v:ViolationCollector):ValidationResult {
		// well-formedness
		if (type == null) { return nullTag(v); }
		if (!Utf16Util.isXmlName(type)) { return elementTypeNotXmlName(v, type); }
		{
			var r:ValidationResult= checkAttributesWellFormed(attr, v);
			if (r != ValidationResult.VALID) { return r; }
		}
		if (!deletionStackIsEmpty()) { return insertInsideDelete(v); }
		
		// validity
		{
			var r:ValidationResult= checkAnnotationsForInsertion(v);
			if (!r.isValid()) { return r; }
		}
		
		// schema
		{
			var r:ValidationResult= validateAttributes(type, attr, v);
			if (r != ValidationResult.VALID) { return r; }
		}
		var parentTag:String= effectiveEnclosingElementTag();
		if (!elementAllowsChild(parentTag, type)) { return invalidChild(v, parentTag, type); }
		{
			var r:ValidationResult= checkForInsertionBeforeRequiredChild(v);
			if (!r.isValid()) { return r; }
		}
		if (nextRequiredElement != null && !(nextRequiredElement == type)) {
			differentElementTypeRequired(v, nextRequiredElement, type);
		}
		return valid();
	}
	
	public function doElementStart(type:String, attr:Attributes):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkElementStart(type, attr, null).isIllFormed());
		}
		updateDeletionTargetAnnotations();
		insertionStackPush(InsertStart.getInstance(type));
		nextRequiredElement = requiredFirstChild(type);
		resultingPos += 1;
		afterAnnotationBoundary = false;
	}
	
	
	public function checkElementEnd(v:ViolationCollector):ValidationResult {
		// well-formedness
		if (!deletionStackIsEmpty()) { return insertInsideDelete(v); }
		if (insertionStackIsEmpty()) { return mismatchedInsertEnd(v); }
		// validity
		{
			var r:ValidationResult= checkAnnotationsForInsertion(v);
			if (!r.isValid()) { return r; }
		}
		// schema
		if (nextRequiredElement != null) {
			childElementRequired(v, nextRequiredElement);
		}
		return valid();
	}
	
	public function doElementEnd():void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkElementEnd(null).isIllFormed());
		}
		updateDeletionTargetAnnotations();
		insertionStackPop();
		resultingPos += 1;
		afterAnnotationBoundary = false;
	}
	
	
	private function attributesEqual(attr:Attributes, bAttr:Attributes):Boolean {
		if (attr.size() != bAttr.size()) { return false; }
		//    Map<String, String> a = attr;
		for (var key:String in attr.keySet()) {
			if (!equal(attr.getValue(key), bAttr.getValue(key))) { return false; }
		}
		return true;
	}
	
	
	public function checkDeleteCharacters(chars:String, v:ViolationCollector):ValidationResult {
		// well-formedness
		if (chars == null) { return nullCharacters(v); }
		if (StrUtil.isEmpty(chars)) { return emptyCharacters(v); }
		if (Utf16Util.firstSurrogate(chars) != -1) { return deleteCharactersContainsSurrogate(v); }
		if (!Utf16Util.isValidUtf16(chars)) { return deleteCharactersInvalidUnicode(v); }
		if (!insertionStackIsEmpty()) { return deleteInsideInsert(v); }
		// validity
		for (var offset:int= 0; offset < chars.length; offset++) {
			var charHereIfAny:int= doc.charAt(effectivePos + offset);
			if (charHereIfAny == -1) {
				return cannotDeleteSoManyCharacters(v, offset, chars);
			}
			var charHere:String= String.fromCharCode(charHereIfAny);
			if (charHere != chars.charAt(offset)) {
				return oldCharacterDiffersFromDocument(v, charHere, chars.charAt(offset));
			}
		}
		return checkAnnotationsForDeletion(v, chars.length);
	}
	
	public function doDeleteCharacters(chars:String):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkDeleteCharacters(chars, null).isIllFormed());
		}
		advance(chars.length);
		afterAnnotationBoundary = false;
	}
	
	
	public function checkDeleteElementStart(type:String, attr:Attributes,
											v:ViolationCollector):ValidationResult {
		// well-formedness
		if (type == null) { return nullTag(v); }
		if (!Utf16Util.isXmlName(type)) { return elementTypeNotXmlName(v, type); }
		{
			var r:ValidationResult= checkAttributesWellFormed(attr, v);
			if (r != ValidationResult.VALID) { return r; }
		}
		if (!insertionStackIsEmpty()) { return deleteInsideInsert(v); }
		// validity
		if (effectiveDocSymbol() != DocSymbol.OPEN) { return noElementStartToDelete(v); }
		if (!effectiveDocSymbolTag() == type) { return oldTagDifferFromDocument(v); }
		if (!attributesEqual(attr, effectiveDocSymbolAttributes())) {
			return oldAttributesDifferFromDocument(v);
		}
		{
			var r:ValidationResult= checkAnnotationsForDeletion(v, 1);
			if (!r.isValid()) { return r; }
		}
		// schema
		if (deletionStackDepth == 0) {
			if (effectivePos < doc.length()) {
				var parentType:String= doc.nthEnclosingElementTag(effectivePos, 0);
				var requiredFirstChild:String= requiredFirstChild(parentType);
				var isFirstChild:Boolean= effectivePos == 0|| doc.elementStartingAt(effectivePos - 1) != null;
				if (isFirstChild && requiredFirstChild != null) {
					return attemptToDeleteRequiredChild(v);
				}
			}
		}
		return valid();
	}
	
	public function doDeleteElementStart(tag:String, attr:Attributes):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkDeleteElementStart(tag, attr, null).isIllFormed());
		}
		deletionStackPush();
		advance(1);
		resultingPos += 1;
		afterAnnotationBoundary = false;
	}
	
	
	public function checkDeleteElementEnd(v:ViolationCollector):ValidationResult {
		// well-formedness
		if (!insertionStackIsEmpty()) { return deleteInsideInsert(v); }
		if (deletionStackIsEmpty()) { return mismatchedDeleteEnd(v); }
		// validity
		if (effectiveDocSymbol() != DocSymbol.CLOSE) { return noElementEndToDelete(v); }
		{
			var r:ValidationResult= checkAnnotationsForDeletion(v, 1);
			if (!r.isValid()) { return r; }
		}
		return valid();
	}
	
	public function doDeleteElementEnd():void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(checkDeleteElementEnd(null) != ValidationResult.ILL_FORMED);
		}
		deletionStackPop();
		advance(1);
		resultingPos += 1;
		afterAnnotationBoundary = false;
	}
	
	
	public function checkUpdateAttributes(u:AttributesUpdate, v:ViolationCollector):ValidationResult {
		// well-formedness
		{
			var r:ValidationResult= checkAttributesUpdateWellFormed(u, v);
			if (!r.isValid()) { return r; }
		}
		if (!deletionStackIsEmpty()) { return attributeChangeInsideInsertOrDelete(v); }
		if (!insertionStackIsEmpty()) { return attributeChangeInsideInsertOrDelete(v); }
		
		// validity
		if (effectiveDocSymbol() != DocSymbol.OPEN) { return noElementStartToChangeAttributes(v); }
		var type:String= effectiveDocSymbolTag();
		org.waveprotocol.wave.model.util.Assert.assert(type != null);
		var oldAttrs:Attributes= effectiveDocSymbolAttributes();
		for (var i:int= 0; i < u.changeSize(); i++) {
			var key:String= u.getChangeKey(i);
			var oldValue:String= u.getOldValue(i);
			if (!equal(oldValue, oldAttrs.getValue(key))) { return oldAttributesDifferFromDocument(v); }
		}
		{
			var r:ValidationResult= checkAnnotationsForRetain(v, 1);
			if (!r.isValid()) { return r; }
		}
		
		// schema
		for (var i:int= 0; i < u.changeSize(); i++) {
			var key:String= u.getChangeKey(i);
			var value:String= u.getNewValue(i);
			if (value != null) {
				if (!elementAllowsAttribute(type, key, value)) {
					return invalidAttribute(v, type, key, value);
				}
			}
		}
		return ValidationResult.VALID;
	}
	
	public function doUpdateAttributes(u:AttributesUpdate):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkUpdateAttributes(u, null).isIllFormed());
		}
		advance(1);
		updateDeletionTargetAnnotations();
		resultingPos += 1;
		afterAnnotationBoundary = false;
	}
	
	
	public function checkReplaceAttributes(oldAttrs:Attributes, newAttrs:Attributes,
										   v:ViolationCollector):ValidationResult {
		// well-formedness
		{
			var r:ValidationResult= checkAttributesWellFormed(oldAttrs, v);
			if (!r.isValid()) { return r; }
		}
		{
			var r:ValidationResult= checkAttributesWellFormed(newAttrs, v);
			if (!r.isValid()) { return r; }
		}
		if (!deletionStackIsEmpty()) { return attributeChangeInsideInsertOrDelete(v); }
		if (!insertionStackIsEmpty()) { return attributeChangeInsideInsertOrDelete(v); }
		
		// validity
		if (effectiveDocSymbol() != DocSymbol.OPEN) { return noElementStartToChangeAttributes(v); }
		var type:String= effectiveDocSymbolTag();
		org.waveprotocol.wave.model.util.Assert.assert(type != null);
		var actualOldAttrs:Attributes= effectiveDocSymbolAttributes();
		if (!attributesEqual(actualOldAttrs, oldAttrs)) { return oldAttributesDifferFromDocument(v); }
		{
			var r:ValidationResult= checkAnnotationsForRetain(v, 1);
			if (!r.isValid()) { return r; }
		}
		
		// schema
		{
			var r:ValidationResult= validateAttributes(type, newAttrs, v);
			if (!r.isValid()) { return r; }
		}
		return valid();
	}
	
	public function doReplaceAttributes(oldAttrs:Attributes, newAttrs:Attributes):void {
		if (EXPENSIVE_ASSERTIONS) {
			org.waveprotocol.wave.model.util.Assert.assert(!checkReplaceAttributes(oldAttrs, newAttrs, null).isIllFormed());
		}
		advance(1);
		updateDeletionTargetAnnotations();
		resultingPos += 1;
		afterAnnotationBoundary = false;
	}
	
	
	/**
	 * Checks whether the automaton is in an accepting state, i.e., whether the
	 * operation would be valid if no further operation components follow.
	 */
	public function checkFinish(v:ViolationCollector):ValidationResult {
		// well-formedness
		if (!insertionStackIsEmpty()) {
			//    	ArrayList<InsertStart>  insertionStack = this.insertionStack;
			for(var i:int = 0; i< insertionStack.length; i++) {
				var e:InsertStart = InsertStart(insertionStack.getItemAt(i));
				return e.notClosed(this, v);
			}
		}
		if (!deletionStackIsEmpty()) {
			return mismatchedDeleteStart(v);
		}
		if (annotationsUpdate.changeSize() > 0) {
			return mismatchedStartAnnotation(v, annotationsUpdate.getChangeKey(0));
		}
		
		// validity
		if (effectivePos != doc.length()) {
			return missingRetainToEnd(v);
		}
		return ValidationResult.VALID;
	}
	
}
}